\documentclass{article} % 声明文档类型为「文章」（适合短篇报告，可选 book/report 等）
\usepackage[UTF8]{ctex} % 加载 ctex 宏包（支持中文），utf8编码
\usepackage{graphicx}
\usepackage{amsmath} % 添加数学包支持

% 自定义 section 编号格式为中文数字
\renewcommand{\thesection}{\chinese{section}}
 % 二级标题用"阿拉伯数字.阿拉伯数字"
\renewcommand{\thesubsection}{\arabic{section}.\arabic{subsection}}


% 文档正文开始（此后内容会被编译显示）
\begin{document} 

\begin{center} % 开启「居中」环境（使内部内容水平居中）
% \tiny（极小）→ \scriptsize → \footnotesize → \small → \normalsize（默认）→ \large → \Large → \LARGE → \huge → \Huge（依次增大）。
% bold font : bf 加粗字体
{\LARGE\textbf{实验三 \ 谓词逻辑的Z语言基本语法与规则}} \\
\vspace{0.5em} % 增加标题与信息间的垂直间距
\normalsize\textbf{
姓名: \underline{\ \normalfont 李豆豆 \ } \ 
学号: \underline{\ \normalfont 202213216 \ } \ 
专业: \underline{\ \normalfont 软件工程 \ } \
评分: \underline{\ \normalfont \quad \quad \quad }
}
\end{center} % 结束居中环境
% \section{}：一级标题（最大层级，自动加粗并编号）；
% \subsection{}：二级标题（缩进，编号如 1.1）；
% \subsubsection{}：三级标题（进一步缩进，编号如 1.1.1）。
\section{实验目的}  % 一级标题（自动编号为 1 实验目的）
会用LaTex编辑谓词逻辑部分的形式化语言，熟悉Z语言的使用，并生成pdf文件。
\section{实验设备}
可上网计算机。
\section{软件工具的实验内容及步骤}
    \subsection{实验内容：}
        \noindent 编辑教材第二章（2.3.5）谓词逻辑中的推理规则。
        \begin{enumerate}
        % \forall表示全称量词
        % \exists表示存在量词
            \item 用于量词公式化的定律
            \item 有关$\forall$的定律：
            \item 有关$\exists$的定律：
            \item 重命名量词变量的定律：
            \item 分离量词化谓词的定律：
            \item 有关非空量词的定律：
        \end{enumerate}
        
    \subsection{实验步骤：}
        \begin{enumerate}
        % \wedge 表示 合取，二者皆成立则成立
        % \frac{m1}{m2} 表示从m1推出m2,也就是m1/m2
        % \dfrac 是升级版
            \item 用于量词公式化的定律：
            % \item \begin{align*} 是 LaTeX 中用于排版多行数学公式的环境，特点是：
            % align 环境用于对齐多行公式
            % * 星号表示不显示公式编号（如果不加星号，每行公式会自动编号）
            % 使用 & 符号来指定对齐点
            % 每行公式用 \\ 来换行
            % [8pt]在每行之前添加适当边距
                \begin{align*}
                    & (\forall x:T \bullet p) \wedge (\forall x:U \bullet q)
                \end{align*}
            \item 有关$\forall$的定律：
                \begin{align*}
                    & \dfrac{(\forall x:T \bullet p),t \in T}{p[t/x]} && \text{SP} \\[8pt]
                    & \dfrac{\forall x,T \bullet P(x)}{P(a)} && \text{(其中$a$是任意的)} \quad \forall\text{-elim} \\[8pt]
                    & \dfrac{P(a)}{\forall x:T \bullet P(x)} && \text{(其中$a$是任意的)} \quad \forall\text{-int}
                \end{align*}
            \item 有关$\exists$的定律：
                \begin{align*}
                    & \dfrac{\exists x:T \bullet P(x)}{P(a)} && \text{($a$是特定标识符号)} \quad \exists\text{-elim} \\[8pt]
                    & \dfrac{P(a)}{\exists x:T \bullet P(x)} && \text{($t$是任意的项)} \quad \exists\text{-int} \\[8pt]
                    & \dfrac{\underline{\exists x:T \bullet p}}{\neg \forall x:T \bullet \neg p} && \text{Def } \exists \\[8pt]
                    & \dfrac{p[t/x],t \in T}{\exists x:T \bullet p} && \exists\text{I} \\[8pt]
                    & \dfrac{\exists x:S \bullet (p \wedge x=t)}{t \in S \wedge p[t/x]} && \text{One-point Rule}
                \end{align*}
            \item 重命名量词变量的定律：
                \begin{align*}
                    & \dfrac{\forall x:T \bullet p}{\forall y:T \bullet p[y/x]} && (y\backslash p,y\backslash T) \quad \text{R}\forall \\[8pt]
                    & \dfrac{\exists x:T \bullet p}{\exists y:T \bullet p[y/x]} && (y\backslash p,y\backslash T) \quad \text{R}\exists
                \end{align*}
            \item 分离量词化谓词的定律：
                \begin{align*}
                    & \dfrac{\underline{\forall x:T \bullet p \wedge q}}{\forall x:T \bullet p \wedge \forall x:T \bullet q} && \text{Q1} \\[8pt]
                    & \dfrac{\underline{\exists x:T \bullet p \vee q}}{\exists x:T \bullet p \vee \exists x:T \bullet q} && \text{Q2} \\[8pt]
                    & \dfrac{\underline{\exists x:T \bullet p \Rightarrow q}}{\forall x:T \bullet p \Rightarrow q} && \text{Q3} \\[8pt]
                    & \dfrac{\underline{\forall x:T \bullet p \Rightarrow q}}{p \Rightarrow \forall x:T \bullet q} && \text{Q4 } (x\backslash p) \\[8pt]
                    & \dfrac{\forall x:T \bullet p \Rightarrow q}{(\exists x:T \bullet p) \Rightarrow q} && \text{Q5 } (x\backslash q) \\[8pt]
                    & \dfrac{(\forall x:T \bullet p) \vee (\forall x:T \bullet q)}{\forall x:T \bullet p \vee q} && \text{Q6} \\[8pt]
                    & \dfrac{\forall x:T \bullet p \Rightarrow q}{\exists x:T \bullet p \Rightarrow \exists x:T \bullet q} && \text{Q7} \\[8pt]
                    & \dfrac{\exists x:T \bullet p \wedge q}{(\exists x:T \bullet p) \wedge (\exists x:T \bullet q)} && \text{Q8}
                \end{align*}
            \item 有关非空量词的定律：
                \begin{align*}
                    & \dfrac{\underline{\forall x:T \bullet p}}{p} && \text{(}x\backslash p\text{,}T\text{非空)} \quad \text{S}\forall \\[8pt]
                    & \dfrac{\underline{\exists x:T \bullet p}}{p} && \text{(}x\backslash p\text{,}T\text{非空)} \quad \text{S}\exists \\[8pt]
                    & \dfrac{\forall x:T \bullet p}{\exists x:T \bullet p} && \text{(}T\text{非空)} \quad \text{Q12} \\[8pt]
                    & \dfrac{(\exists x:T \bullet p) \Rightarrow (\exists x:T \bullet q)}{\exists x:T \bullet p \Rightarrow q} && \text{(}T\text{非空)} \quad \text{Q13}
                \end{align*}
        \end{enumerate}
    
    \subsection{实验心得：}
        \indent 通过本次实验，我深入学习了LaTeX中数学公式的排版方法，特别是在处理谓词逻辑的各种推理规则时，掌握了量词、逻辑符号的输入方法。在实验过程中，我认识到了align*环境在对齐公式时的重要性，以及如何使用\verb|\text{}|来在数学环境中插入文字说明。这些技能对于今后编写数学相关的文档都很有帮助。同时，通过编写这些推理规则，也加深了我对谓词逻辑本身的理解。
\end{document}